\begin{tabbing}
es{-}copies(${\it es}$;$e$;$x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$\=$a$:Atom1\+
\\[0ex](es{-}atom(${\it es}$;es{-}loc(${\it es}$; $e$);$a$)
\\[0ex]\& (\=$\neg$free{-}from{-}atom\{1\}(es{-}vartype(${\it es}$; es{-}loc(${\it es}$; $e$); $x$);es{-}when\+
\\[0ex](${\it es}$; $x$; es{-}init(${\it es}$;$e$));$a$))
\-\\[0ex]\& free{-}from{-}atom\{1\}(es{-}state{-}without(${\it es}$;es{-}loc
\\[0ex](${\it es}$; $e$);$x$);es{-}state{-}when{-}without(${\it es}$;$e$;$x$);$a$)
\\[0ex]\& es{-}rcv{-}atom(${\it es}$;$e$;$a$)
\\[0ex]\& (\=$\neg$free{-}from{-}atom\{1\}(es{-}state{-}without(${\it es}$;es{-}loc\+
\\[0ex](${\it es}$; $e$);$x$);es{-}state{-}after{-}without(${\it es}$;$e$;$x$);$a$)))
\-\-
\end{tabbing}